:- dynamic globalFrozenCount/1.

globalFrozenFunctor(frozen___).

freeze_term(Term) :-
	freeze_term(Term, Term).

freeze_predicate(Pred, N, Frozen) :-
	functor(Term, Pred, N),
	freeze_term(Term, Frozen).

freeze_predicate(Predicate, Frozen) :-
	current_functor(Predicate, N),
	freeze_predicate(Predicate, N, Frozen).

freeze_term(Term, Frozen) :-
	globalFrozenFunctor(F),
	freeze_term(Term, Frozen, F).

freeze_term(Term, Frozen, Functor) :-
	globalFrozenCount(N),
	!,
	freeze_term(Term, Frozen, N, Functor).
freeze_term(Term, Frozen, Functor) :-
	freeze_term(Term, Frozen, 1, Functor).


skolem_predicate(Predicate, Arity, Skolemized) :-
	functor(Term, Predicate, Arity),
	skolem_term(Term, Skolemized).

%% freeze_term(+Term, -FrozenTerm, +StartCount, +FunctorName) :
%% freeze the given Term using the given functor name and starting count into FrozenTerm
freeze_term(Term, Frozen, Start, Functor) :-
	copy_term(Term, Frozen),
	numbervars(Frozen, Start, End, [functor_name(Functor)]),
	setFrozenCount(End).

setFrozenCount(N) :-
	integer(N),
	retractall(globalFrozenCount(_)),
	assert(globalFrozenCount(N)).

resetFrozenCount :-
	setFrozenCount(1).


skolem_term(Term, Skolemized) :-
	genSkolemFunctor(F),
	skolem_term(Term, Skolemized, F).

skolem_term(Term, Skolemized, Functor) :-
	globalFrozenCount(N),
	!,
	skolem_term(Term, Skolemized, N, Functor).
skolem_term(Term, Skolemized, Functor) :-
	skolem_term(Term, Skolemized, 1, Functor).


skolem_term(Term, Skolemized, Start, Functor) :-
	copy_term(Term, Skolemized),
	numbervars(Skolemized, Start, End, [functor_name(Functor)]),
	setFrozenCount(End).

%%   Frozen has to be ground!
melt_term(Frozen, Term) :-
	globalFrozenFunctor(F),
	melt_term(Frozen, Term, F).
	
%% melt_term(+Frozen, -Term, +Functor): melt the frozen term using variables indicated by the provided functor
melt_term(Frozen, Term, Functor) :-
	melt(Frozen, Term, Functor, Dict),
	!.



melt(X, X, Functor, Dict) :-
	atomic(X),
	!.

melt(Var, X, Functor, Dict) :-
	Var =.. [Functor,N],
	!,
	lookup(N, Dict, X).


melt(X, Y, Functor, Dict) :-
	compound(X),
	functor(X, F, N),
	functor(Y, F, N),
	F \== Functor,
	melt(N, X, Y, Functor, Dict).




melt(N, X, Y, Functor, Dict) :-
	N > 0,
	!,
	arg(N, X, ArgX),
	melt(ArgX, ArgY, Functor, Dict),
	arg(N, Y, ArgY),
	N1 is N-1,
	melt(N1, X, Y, Functor, Dict).

melt(0, X, Y, Functor, Dict).

%%	dictionary lookup in binary search tree
lookup(Key, dict(Key, X, Left, Right), Value) :-
	!,
	X = Value.

lookup(Key, dict(Key1, X, Left, Right), Value) :-
	Key < Key1,
	!,
	lookup(Key, Left, Value).

lookup(Key, dict(Key1, X, Left, Right), Value) :-
	Key > Key1,
	lookup(Key, Right, Value).




%% create a new functor with the global skolem prefix and the frozen counter
genSkolemFunctor(F) :-
	genSkolemFunctor(F, skolem).

genSkolemFunctor(F, Name) :-
	nextFrozenCount(N),
	concat_atom([Name,N],'___', F).

nextFrozenCount(N) :-
	globalFrozenCount(N),
	!,
	N1 is N+1,
	setFrozenCount(N1).

nextFrozenCount(N) :-
	setFrozenCount(101),
	N is 101.%% set to default starting num.


%%   skolemize rule head using global skolem functor.
skolemize((H,B), (NH, NB, OH)) :-
	term_variables(H, HV),
	term_variables(B, BV),
	freeze_term((H,B,HV,BV), (FH,FB, FHV, FBV)),
	intersection(FHV, FBV, CommenVars),
	skolemize_ground((FNH,FNB),(FH,FB),FHV,CommenVars),
	!,
	melt_term((FNH, FNB, FH),(NH, NB, OH)).


% BVars is a non-empty ground list.
% skolemize_ground(NRule, Rule, HeadVars, CommenVars)
skolemize_ground(Rule, Rule, [], BVars).

skolemize_ground(NRule, Rule, [H|T], BVars) :-
	member(H,BVars),
	!,
	skolemize_ground(NRule, Rule, T, BVars).

skolemize_ground(NRule, Rule, [H|T], BVars) :-
	genSkolemFunctor(F),
	New =.. [F|BVars],
	substitute(H, New, Rule, Rule1),
	skolemize_ground(NRule, Rule1, T, BVars).


intersection([X|Y],M,[X|Z]) :-
	member(X,M),
	intersection(Y,M,Z).

intersection([X|Y],M,Z) :-
	\+ member(X,M),
	intersection(Y,M,Z).

intersection([],M,[]).

%% ground input only!
%nonmember(X, [Y|Ys]) :- X \= Y, nonmember(X, Ys).
%nonmember(X, []).


%%	Old can be non-ground, while X and Y have to be ground.
non_ground_substitute(X, Y, Old, New) :-
	freeze_term(Old, Old1),
	substitute(X, Y, Old1, Old2),
	melt_term(Old2, New).

%%%
% substitute(Old, New, OldTerm, NewTerm): both Old and New should be
% ground! OldTerm should also be ground.
substitute(Old, New, Old, New) :-
	!.

substitute(Old, New, Term, Term) :-
	atomic(Term),
	!,
	Term \== Old.

substitute(Old, New, OldTerm, NewTerm) :-
	compound(OldTerm),
	functor(OldTerm, F,N),
	functor(NewTerm, F, N),
	substitute(N, Old, New, OldTerm, NewTerm).

substitute(N, Old, New, OldTerm, NewTerm) :-
	N > 0,
	!,
	arg(N, OldTerm, Arg),
	substitute(Old, New, Arg, Arg1),
	arg(N, NewTerm, Arg1),
	N1 is N-1,
	substitute(N1, Old, New, OldTerm, NewTerm).

substitute(0, Old, New, OldTerm, NewTerm).
